E,X1,X2:Type, info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), pred?:(E(?E)), e,e':E.
pred!(e;e')  prop{i:l} 

latex

Definitions	x:A. B(x), t  T, prop{i:l}, pred!(e;e'), P  Q, A c B, top, subtype(S; T), suptype(S; T), P  Q
Lemmas	not wf, assert wf, first wf, top wf, unit wf, pred wf, rcv? wf, sender wf, Id wf, IdLnk wf